00100	                    ON ADDING QUANTIFIERS TO LCS

00200	
00300	                          by John McCarthy
00400	
00500	
00600		It is clearly desirable to  add  quantifiers  to  LCS,  since
00700	without  them  some  important  facts  are  unstatable and a fortiori
00800	unprovable. Here is  a  safe  way  to  do  it  even,  if  it  is  not
00900	necessarily the most powerful.
01000	
01100		We  adjoin  to  the  language  a  new  class of predicate and
01200	function  symbols  called  external  symbols.   These   symbols   are
01300	distinguished  by  either  a  typographical convention, presence on a
01400	special list, or by declaration.  They  are  not  allowed  to  appear
01500	within  an LCF formula, i.e. a formula that can appear as an argument
01600	of the ⊂-relation or as an argument of the α-operator.  They can take
01700	these  any  LCF  expressions as arguments. Quantification is over LCF
01800	objects.  Idea: it might be worthwhile to take the ⊂-relation  as  an
01900	external  predicate, and use ordinary logic from that point outwards.
02000	This allows "monotonic", "continuous", etc. to be external predicates
02100	in the language.